A list is a (possibly infinite) sequence of values. For example,
the list [1, 2, 3] contains three numbers, the list [ ] contains
none, and the list #math118#[1, 2, 3,…] contains infinitely many.
A list is either <#224#>empty<#224#> (written [ ]) or is comprised
of a <#225#>head<#225#>
x and a <#226#>tail<#226#> xs (in which case it's written x : xs).
For example, #math119#1 : 2 : 3 : [ ] is [1, 2, 3].
In a similar fashion to the implementation of booleans,
a list xs is implemented as a function of the form
#math120#
| xs~f~e |
= |
#tex2html_wrap_indisplay2361##tex2html_wrap_indisplay2362# |
|
Again, we are implementing a datatype as a function, a quite powerful
trick, just not one usually seen in TEX. We will assume that
whenever a list x : xs is applied to f and e, f~x respects equality.
This allows us to assume that if xs = ys then #math121#x : xs = x : ys,
which is handy.